package trabajoISW2.domain.contracts;

import tdg.contract.semanticAnnotations.Inv;
import tdg.contract.semanticAnnotations.Pos;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Query;
import trabajoISW2.domain.implementations.CreditCard;
import trabajoISW2.domain.implementations.Order;


@Inv("getInvoicedId() >= 0")
public interface IInvoice {
	
	@Query
	public void showInvoice();
	
	@Pre("order != null #IllegalArgumentException")
	@Pos("getOrder().compare(order) == 0")
	public void setOrder(Order order);
	
	@Query
	public Order getOrder();
	
	@Pre("card != null #IllegalArgumentException")
	@Pos("getCreditCard().compare(card) == 0")
	public void setCreditCard (CreditCard card);
	
	@Query
	public CreditCard getCreditCard();
	
}
